$\forall$$A$, $B$:Type, $a$:EqDecider($A$), $b$:EqDecider($B$). sumdeq($a$;$b$) $\in$ ($A$+$B$)$\rightarrow$($A$+$B$)$\rightarrow\mathbb{B}$